/LMAR=0/XLINE=10/FONT#0=NONM/FONT#1=BASI30/FONT#2=NONMB/FONT#3=MATHX[PUB,PAT]/FONT#5=FORN25/FONT#6=FIX25/FONT#7=MISC25/FONT#8=PLUNK/FONT#9=GRFX25/FONT#10=BASB30/FONT#11=CLAR30/FONT#12=MATH50/FONT#13=FIX20/FONT#14=CLAR40/TMAR=200/PMAR=1900/BMAR=100


␈↓"β␈↓ α∧␈↓␈↓ ¬∞␈↓αII. BIOGRAPHICAL INFORMATION ␈↓

␈↓"β␈↓ α∧␈↓Name:  ␈↓αZohar Manna␈↓
␈↓"β␈↓ α∧␈↓Born:  January 17, 1939 (Haifa, Israel)
␈↓"β␈↓ α∧␈↓Dual citizenship:  Israel and United States


␈↓"β␈↓ α∧␈↓␈↓β⊗␈↓  ␈↓αEducation and Work:␈↓

␈↓ α∧␈↓1958␈↓¬-␈↓1962␈↓ β4Undergraduate Student
␈↓ α∧␈↓␈↓ β4Mathematics Department
␈↓ α∧␈↓␈↓ β4Technion, Haifa, Israel
␈↓ α∧␈↓␈↓ β4B.Sc. (1962)

␈↓ α∧␈↓1962␈↓¬-␈↓1964␈↓ β4Israel Defense Forces
␈↓ α∧␈↓␈↓ β4First Lieutenant
␈↓ α∧␈↓␈↓ β4Scientific Programming

␈↓ α∧␈↓1964␈↓¬-␈↓1965␈↓ β4Graduate Student
␈↓ α∧␈↓␈↓ β4Mathematics Department
␈↓ α∧␈↓␈↓ β4Technion, Haifa, Israel
␈↓ α∧␈↓␈↓ β4M.Sc. (1965)

␈↓ α∧␈↓1965␈↓¬-␈↓1968␈↓ β4Graduate Student
␈↓ α∧␈↓␈↓ β4Computer Science Department
␈↓ α∧␈↓␈↓ β4Carnegie␈↓¬-␈↓Mellon University
␈↓ α∧␈↓␈↓ β4Pittsburgh, Pennsylvania
␈↓ α∧␈↓␈↓ β4Ph.D. (1968)

␈↓ α∧␈↓1968␈↓¬-␈↓1971␈↓ β4Assistant Professor
␈↓ α∧␈↓␈↓ β4Computer Science Department
␈↓ α∧␈↓␈↓ β4Stanford University
␈↓ α∧␈↓␈↓ β4Stanford, California

␈↓ α∧␈↓1971␈↓¬-␈↓1972␈↓ β4Visiting Associate Professor
␈↓ α∧␈↓␈↓ β4Computer Science Dept.
␈↓ α∧␈↓␈↓ β4Stanford University
␈↓ α∧␈↓␈↓ β4Stanford, California




␈↓"β␈↓ α∧␈↓␈↓ εj1␈↓ d


␈↓"β␈↓ α∧␈↓1972␈↓¬-␈↓1976␈↓ β4Associate Professor
␈↓ α∧␈↓␈↓ β4Applied Mathematics Dept.
␈↓ α∧␈↓␈↓ β4Weizmann Institute
␈↓ α∧␈↓␈↓ β4Rehovot, Israel

␈↓ α∧␈↓1976␈↓¬-␈↓␈↓ β4Professor␈↓ εT1975␈↓¬-␈↓    ␈↓ πtResearch Associate
␈↓ α∧␈↓␈↓ β4Applied Mathematics Dept.␈↓ εT␈↓ πtArtificial Intelligence Lab
␈↓ α∧␈↓␈↓ β4Weizmann Institute␈↓ εT␈↓ πtStanford University
␈↓ α∧␈↓␈↓ β4Rehovot, Israel␈↓ εT␈↓ πtStanford, California



␈↓"β␈↓ α∧␈↓␈↓β⊗␈↓  ␈↓αScholarships and academic honors␈↓
␈↓"β␈↓ α∧␈↓Undergraduate study ␈↓¬-␈↓ cum laude
␈↓"β␈↓ α∧␈↓HTI Graduate Scholarship
␈↓"β␈↓ α∧␈↓Landau Science Award (1976)


␈↓"β␈↓ α∧␈↓␈↓β⊗␈↓  ␈↓αMemberships␈↓
␈↓"β␈↓ α∧␈↓Association for Computer Machinery
␈↓"β␈↓ α∧␈↓The Insitute of Electrical and Electronics Engineers
␈↓"β␈↓ α∧␈↓European Association for Theoretical Computer Science


␈↓"β␈↓ α∧␈↓␈↓β⊗␈↓  ␈↓αAssociate Editor of:␈↓
␈↓"β␈↓ α∧␈↓Computer Languages Journal
␈↓"β␈↓ α∧␈↓Acta Informatica
␈↓"β␈↓ α∧␈↓Theoretical Computer Science Journal


␈↓"β␈↓ α∧␈↓␈↓β⊗␈↓  ␈↓αResearch Interests:␈↓
␈↓"β␈↓ α∧␈↓Mathematical Theory of Computation
␈↓"β␈↓ α∧␈↓Program Verification and Synthesis
␈↓"β␈↓ α∧␈↓Methodology of Programming
␈↓"β␈↓ α∧␈↓Programming Languages


␈↓"β␈↓ α∧␈↓␈↓β⊗␈↓  ␈↓αSpecial Committees␈↓

␈↓"β␈↓ α∧␈↓Council member of the European Association for Theoretical Computer Science

␈↓"β␈↓ α∧␈↓Member␈αof␈αthe␈αTheory␈αof␈αComputing␈αPanel␈αof␈αthe␈αNSF␈αComputer␈αScience␈αand␈αEngineering
␈↓ α∧␈↓Research Study.


␈↓"β␈↓ α∧␈↓␈↓ εj2␈↓ d


␈↓"β␈↓ α∧␈↓␈↓β⊗␈↓  ␈↓αPublic Service␈↓
␈↓"β␈↓ α∧␈↓        1. Member of the Theory of Computing Panel of the NSF Computer
␈↓"β␈↓ α∧␈↓Science and Engineering Research Study (COSERS).
␈↓"β␈↓ α∧␈↓α        2. Council member of the European Association for Theoretical
␈↓"β␈↓ α∧␈↓αComputer Science.

␈↓"β␈↓ α∧␈↓α        3. Member of IFIP 2.2 working group: Formal description of
␈↓"β␈↓ α∧␈↓αprogramming concepts.

␈↓"β␈↓ α∧␈↓α        4. Member of program committee of about 12 conferences.

␈↓"β␈↓ α∧␈↓α        5. Associate editor of three journals: Computer Language Journal,
␈↓"β␈↓ α∧␈↓αActa Informatica, and Theoretical Computer Science Journal.


␈↓"β␈↓ α∧␈↓␈↓β⊗␈↓  ␈↓αCurrent Grants/Contracts:␈↓

␈↓"β␈↓ α∧␈↓At␈α⊂Stanford␈α∂University:␈α⊂National␈α∂Science␈α⊂Foundation␈α∂(Grant␈α⊂MCS␈α∂76␈↓¬-␈↓83655)␈α⊂Office␈α∂of
␈↓ α∧␈↓Naval␈α⊂Research␈α⊂(Contract␈α⊃NOOO14␈↓¬-␈↓76␈↓¬-␈↓C␈↓¬-␈↓0687)␈α⊂Advanced␈α⊂Research␈α⊃Projects␈α⊂Agency
␈↓ α∧␈↓(Part of Contract MDA 903␈↓¬-␈↓76␈↓¬-␈↓C␈↓¬-␈↓0206)

␈↓"β␈↓ α∧␈↓At␈αthe␈α
Weizmann␈αInstitute:␈α
United␈αStates␈αAir␈α
Force␈αOffice␈α
of␈αScientific␈α
Research␈α(Grant
␈↓ α∧␈↓AFOSR␈↓¬-␈↓76␈↓¬-␈↓2909) United States␈↓¬-␈↓Israel Binational Science Foundation (Grant 574)


␈↓"β␈↓ α∧␈↓␈↓β⊗␈↓  ␈↓αMajor invited papers and addresses␈↓

␈↓"β␈↓ α∧␈↓1.  ␈↓↓Automatic␈α∞programming␈↓,␈α∞Third␈α∞International␈α
Joint␈α∞Conference␈α∞on␈α∞Artificial␈α
Intelligence,
␈↓ α∧␈↓Stanford, CA (August 1973).

␈↓"β␈↓ α∧␈↓2.  ␈↓↓Towards␈α⊃automatic␈α⊃debugging␈α⊃of␈α⊂programs␈↓,␈α⊃First␈α⊃International␈α⊃Conference␈α⊃on␈α⊂Reliable
␈↓ α∧␈↓Software, Los Angeles, CA (April 1975).

␈↓"β␈↓ α∧␈↓3.  ␈↓↓On␈α~automating␈α→structured␈α~programming␈↓,␈α~International␈α→Symposium␈α~on␈α~Proving␈α→and
␈↓ α∧␈↓Improving Programs, Arc␈↓¬-␈↓et␈↓¬-␈↓Senans, France (July 1975).

␈↓"β␈↓ α∧␈↓4.  ␈↓↓The␈α∨recursive␈α≡way␈α∨of␈α≡thinking␈↓,␈α∨Carnegie␈↓¬-␈↓Mellon␈α≡University␈α∨Computer␈α≡Science
␈↓ α∧␈↓Department 10␈↓#
[␈↓#th] Anniversary Symposium, Pittsburgh, PA (October 1975).

␈↓"β␈↓ α∧␈↓5.  ␈↓↓Intermittent␈α∞assertions␈α∞in␈α∂proving␈α∞program␈α∞correctness␈↓,␈α∞Second␈α∂International␈α∞Conference
␈↓ α∧␈↓on Software Engineering, San Francisco, CA (October 1976).

␈↓"β␈↓ α∧␈↓6.  ␈↓↓New␈α
trends␈α
in␈αprogram␈α
verification␈↓,␈α
Computer␈αScience␈α
Conference,␈α
Atlanta,␈αGA␈α
(January
␈↓ α∧␈↓1977).

␈↓"β␈↓ α∧␈↓␈↓ εj3␈↓ d


␈↓"β␈↓ α∧␈↓7.  ␈↓↓The␈α
fixedpoint␈α
theory␈α
of␈αrecursive␈α
programs␈↓,␈α
American␈α
Mathematical␈α
Society␈αMeeting,␈α
San
␈↓ α∧␈↓Luis Obispo, CA (November 1977).

␈↓"β␈↓ α∧␈↓8.  ␈↓↓Program␈α~verification␈α~without␈α≠magic␈↓,␈α~Third␈α~International␈α~Conference␈α≠on␈α~Software
␈↓ α∧␈↓Engineering, Atlanta, GA (May 1978).

␈↓"β␈↓ α∧␈↓9.  ␈↓↓The DEDALUS system␈↓, National Computer Conference, Anaheim, CA (June 1978).



































␈↓"β␈↓ α∧␈↓␈↓ εj4␈↓ d


␈↓"β␈↓ α∧␈↓␈↓ ∧z␈↓αIII. BIBLIOGRAPHICAL INFORMATION␈↓

␈↓ α∧␈↓1.␈↓ αdZ. Manna [April 1969]
␈↓ α∧␈↓␈↓ αd␈↓↓Properties␈α∂of␈α∂programs␈α⊂and␈α∂the␈α∂first␈↓␈↓¬-␈↓␈↓↓order␈α⊂predicate␈α∂calculus␈↓,␈α∂␈↓αJournal␈α⊂of␈α∂the
␈↓ α∧␈↓α␈↓ αdACM␈↓, Vol. 16, No. 2, pp. 244␈↓¬-␈↓255.

␈↓ α∧␈↓2.␈↓ αdZ. Manna [May 1969]
␈↓ α∧␈↓␈↓ αd␈↓↓The␈α⊂correctness␈α⊂of␈α⊂programs␈↓,␈α⊂␈↓αJournal␈α⊂of␈α⊂Computer␈α⊂and␈α⊃System␈α⊂Sciences␈↓,
␈↓ α∧␈↓␈↓ αdVol. 3, No. 2, pp. 119␈↓¬-␈↓127.

␈↓ α∧␈↓3.␈↓ αdZ. Manna [May 1970]
␈↓ α∧␈↓␈↓ αd␈↓↓Termination␈αof␈αalgorithms␈αrepresented␈αas␈αinterpreted␈αgraphs␈↓,␈αAFIPS␈αConference
␈↓ α∧␈↓␈↓ αdProceedings, Vol. 36, pp. 83␈↓¬-␈↓90.

␈↓ α∧␈↓4.␈↓ αdZ. Manna [May 1970]
␈↓ α∧␈↓␈↓ αd␈↓↓Second␈↓␈↓¬-␈↓␈↓↓order␈α∀mathematical␈α∀theory␈α∀of␈α∀computation␈↓,␈α∀Proceedings␈α∀of␈α∃the␈α∀ACM
␈↓ α∧␈↓␈↓ αdSymposium on Theory of Computing, pp. 158␈↓¬-␈↓168.

␈↓ α∧␈↓5.␈↓ αdZ. Manna and A. Pnueli [July 1970]
␈↓ α∧␈↓␈↓ αd␈↓↓Formalization␈α∞of␈α∞properties␈α∂of␈α∞functional␈α∞programs␈↓,␈α∂␈↓αJournal␈α∞of␈α∞the␈α∂ACM␈↓,␈α∞Vol.
␈↓ α∧␈↓␈↓ αd17, No. 3, pp. 555␈↓¬-␈↓569.

␈↓ α∧␈↓6.␈↓ αdZ. Manna [1970]
␈↓ α∧␈↓␈↓ αd␈↓↓The␈α∂correctness␈α⊂of␈α∂non␈↓␈↓¬-␈↓␈↓↓deterministic␈α∂programs␈↓,␈α⊂␈↓αArtificial␈α∂Intelligence␈↓,␈α⊂Vol.␈α∂1,
␈↓ α∧␈↓␈↓ αdNo. 1, pp. 1␈↓¬-␈↓26.

␈↓ α∧␈↓7.␈↓ αdZ. Manna and J. McCarthy [1970]
␈↓ α∧␈↓␈↓ αd␈↓↓Properties␈α∪of␈α∪programs␈α∪and␈α∩partial␈α∪function␈α∪logic␈↓,␈α∪␈↓αMachine␈α∪Intelligence␈α∩5␈↓
␈↓ α∧␈↓␈↓ αd(Eds. Meltzer and Michie), Edinburgh University Press, pp. 79␈↓¬-␈↓98.

␈↓ α∧␈↓8.␈↓ αdZ. Manna and R. Waldinger [March 1971]
␈↓ α∧␈↓␈↓ αd␈↓↓Toward␈αautomatic␈αprogram␈α
synthesis␈↓,␈α␈↓αCommunication␈αof␈α
the␈αACM␈↓,␈αVol.␈α14,␈α
No.
␈↓ α∧␈↓␈↓ αd3, pp. 151␈↓¬-␈↓165.

␈↓ α∧␈↓9.␈↓ αdZ. Manna [June 1971]
␈↓ α∧␈↓␈↓ αd␈↓↓Mathematical␈α
theory␈α
of␈α
partial␈α
correctness␈↓,␈α
␈↓αJournal␈α
of␈α
Computer␈α∞and␈α
System
␈↓ α∧␈↓α␈↓ αdSciences␈↓, Vol. 5, No. 3, pp. 239␈↓¬-␈↓253.

␈↓ α∧␈↓10.␈↓ αdE. Ashcroft and Z. Manna [1971]
␈↓ α∧␈↓␈↓ αd␈↓↓Formalization␈αof␈αproperties␈αof␈αparallel␈αprograms␈↓,␈α␈↓αMachine␈αIntelligence␈α6␈↓␈α(Eds.
␈↓ α∧␈↓␈↓ αdMeltzer and Michie), Edinburgh University Press, pp. 17␈↓¬-␈↓41.

␈↓"β␈↓ α∧␈↓␈↓ εj5␈↓ d


␈↓"β␈↓ α∧␈↓11.␈↓ αdJ. M. Cadiou and Z. Manna [January 1972]
␈↓ α∧␈↓␈↓ αd␈↓↓Recursive␈α
definitions␈α
of␈α
partial␈αfunctions␈α
and␈α
their␈α
computations␈↓,␈αProceedings␈α
of
␈↓ α∧␈↓␈↓ αdthe␈α⊂ACM␈α⊂Conference␈α⊂on␈α∂Proving␈α⊂Assertions␈α⊂about␈α⊂Programs,␈α⊂Las␈α∂Cruces,
␈↓ α∧␈↓␈↓ αdNew Mexico, pp. 58␈↓¬-␈↓65.

␈↓ α∧␈↓12.␈↓ αdA. Chandra and Z. Manna [May 1972]
␈↓ α∧␈↓␈↓ αd␈↓↓Program␈α
schemas␈αwith␈α
equality␈↓,␈αProceedings␈α
of␈α
the␈αACM␈α
Symposium␈αon␈α
Theory
␈↓ α∧␈↓␈↓ αdof Computing, pp. 52␈↓¬-␈↓64.

␈↓ α∧␈↓13.␈↓ αdZ. Manna [May 1972]
␈↓ α∧␈↓␈↓ αd␈↓↓Computation␈α∀of␈α∀recursive␈α∀programs␈↓␈α∪␈↓¬-␈↓␈α∀␈↓↓theory␈α∀vs␈α∀practice␈↓,␈α∀AFIPS␈α∪Conference
␈↓ α∧␈↓␈↓ αdProceedings, Vol. 40, pp. 219␈↓¬-␈↓223.

␈↓ α∧␈↓14.␈↓ αdZ. Manna and J. Vuillemin [July 1972]
␈↓ α∧␈↓␈↓ αd␈↓↓Fixpoint␈α
approach␈αto␈α
the␈αtheory␈α
of␈αcomputation␈↓,␈α
␈↓αCommunications␈αof␈α
the␈αACM␈↓,
␈↓ α∧␈↓␈↓ αdVol.␈α⊂15,␈α⊂No.␈α⊂7,␈α⊂pp.␈α⊂528␈↓¬-␈↓536.␈α⊂Invited␈α⊂paper␈α⊂␈↓¬-␈↓␈α⊂␈↓αspecial␈α⊂25th␈α⊂anniversary
␈↓ α∧␈↓α␈↓ αdissue␈↓.

␈↓ α∧␈↓15.␈↓ αdE. Ashcroft, Z. Manna and A. Pnueli [July 1973]
␈↓ α∧␈↓␈↓ αd␈↓↓Decidable␈α∞properties␈α∞of␈α∂monadic␈α∞functional␈α∞schemas␈↓,␈α∂␈↓αJournal␈α∞of␈α∞the␈α∂ACM␈↓,␈α∞Vol.
␈↓ α∧␈↓␈↓ αd20, No. 3, pp. 489␈↓¬-␈↓499.

␈↓ α∧␈↓16.␈↓ αdZ. Manna, S. Ness and J. Vuillemin [August 1973]
␈↓ α∧␈↓␈↓ αd␈↓↓Inductive␈α
methods␈α
for␈αproving␈α
properties␈α
of␈αprograms␈↓,␈α
␈↓αCommunications␈α
of␈αthe
␈↓ α∧␈↓α␈↓ αdACM␈↓,␈α~Vol.␈α→16,␈α~No.␈α~8,␈α→pp.␈α~491␈↓¬-␈↓502.␈α→ACM␈α~Programming␈α~System␈α→and
␈↓ α∧␈↓␈↓ αdLanguages ␈↓¬-␈↓ ␈↓αBest paper Award for 1974␈↓.

␈↓ α∧␈↓17.␈↓ αdS. Katz and Z. Manna [August 1973]
␈↓ α∧␈↓␈↓ αd␈↓↓A␈α→heuristic␈α_approach␈α→to␈α_program␈α→verification␈↓,␈α_Proceedings␈α→of␈α→the␈α_Third
␈↓ α∧␈↓␈↓ αdInternational␈α
Joint␈α
Conference␈αon␈α
Artificial␈α
Intelligence,␈αStanford,␈α
California,
␈↓ α∧␈↓␈↓ αdpp. 500␈↓¬-␈↓512.

␈↓ α∧␈↓18.␈↓ αdZ. Manna and A. Pnueli [1974]
␈↓ α∧␈↓␈↓ αd␈↓↓Axiomatic approach to total correctness␈↓, ␈↓αActa Informatica␈↓, Vol. 3, pp. 243␈↓¬-␈↓263.

␈↓ α∧␈↓19.␈↓ αdS. Katz and Z. Manna [April 1975]
␈↓ α∧␈↓␈↓ αd␈↓↓Towards␈α⊂automatic␈α⊂debugging␈α⊂of␈α∂programs␈↓,␈α⊂Proceedings␈α⊂of␈α⊂the␈α∂International
␈↓ α∧␈↓␈↓ αdConference on Reliable Software, Los Angeles, California. ␈↓αInvited paper␈↓.

␈↓ α∧␈↓20.␈↓ αdE. Ashcroft and Z. Manna [June 1975]


␈↓"β␈↓ α∧␈↓␈↓ εj6␈↓ d


␈↓"β␈↓ α∧␈↓␈↓ αd␈↓↓Translating␈α∂program␈α∞schemas␈α∂to␈α∞while␈↓␈↓¬-␈↓␈↓↓schemas␈↓,␈α∂␈↓αSIAM␈α∞Journal␈α∂on␈α∞Computing␈↓,
␈↓ α∧␈↓␈↓ αdVol. 4, No. 2, pp. 125␈↓¬-␈↓146.

␈↓ α∧␈↓21.␈↓ αdN. Dershowitz and Z. Manna [July 1975]
␈↓ α∧␈↓␈↓ αd␈↓↓On␈α∃automating␈α∃structured␈α⊗programming␈↓,␈α∃Proceedings␈α∃of␈α⊗the␈α∃International
␈↓ α∧␈↓␈↓ αdSymposium␈αon␈αProving␈αand␈αImproving␈αPrograms,␈αArc␈↓¬-␈↓et␈↓¬-␈↓Senans,␈αFrance,␈αpp.
␈↓ α∧␈↓␈↓ αd167␈↓¬-␈↓193.  ␈↓αInvited paper.␈↓

␈↓ α∧␈↓22.␈↓ αdA. Chandra and Z. Manna [September 1975]
␈↓ α∧␈↓␈↓ αd␈↓↓On␈α∞the␈α∞power␈α∞of␈α∞programming␈α∞features␈↓,␈α∞␈↓αComputer␈α∞Languages␈↓,␈α∞Vol.␈α∞1,␈α∂No.␈α∞3,
␈↓ α∧␈↓␈↓ αdpp. 219␈↓¬-␈↓232.

␈↓ α∧␈↓23.␈↓ αdZ. Manna and R. Waldinger [1975]
␈↓ α∧␈↓␈↓ αd␈↓↓Knowledge␈α
and␈α
reasoning␈α
in␈α
program␈α
synthesis␈↓,␈α
␈↓αArtificial␈α
Intelligence␈↓,␈α
Vol.␈α
6,
␈↓ α∧␈↓␈↓ αdNo. 2, pp. 175␈↓¬-␈↓208.

␈↓ α∧␈↓24.␈↓ αdS. Katz and Z. Manna [1975]
␈↓ α∧␈↓␈↓ αd␈↓↓A␈α
closer␈α
look␈α
at␈α
termination␈↓,␈α
␈↓αActa␈αInformatica␈↓,␈α
Vol.␈α
5,␈α
pp.␈α
333␈↓¬-␈↓352.␈α
 Also␈αin
␈↓ α∧␈↓␈↓ αd␈↓↓Current␈α
Trends␈α
in␈α
Programming␈α
Methodology␈↓,␈α
␈↓↓Vol.␈α
II␈↓:␈α
 ␈↓↓Program␈α
Verification␈↓␈α
(R.
␈↓ α∧␈↓␈↓ αdYeh, editor), Prentice␈↓¬-␈↓Hall Inc., 1977.

␈↓ α∧␈↓25.␈↓ αdS. Katz and Z. Manna [April 1976]
␈↓ α∧␈↓␈↓ αd␈↓↓Logical␈α∂analysis␈α∂of␈α∂programs␈↓,␈α∂␈↓αCommunications␈α∞of␈α∂the␈α∂ACM␈↓,␈α∂Vol.␈α∂19,␈α∂No.␈α∞4,
␈↓ α∧␈↓␈↓ αdpp.188␈↓¬-␈↓206.

␈↓ α∧␈↓26.␈↓ αdZ. Manna and A. Shamir [Spetember 1976]
␈↓ α∧␈↓␈↓ αd␈↓↓The␈α
theoretical␈α
aspects␈α
of␈α
the␈α
optimal␈α
fixedpoint␈↓,␈α
␈↓αSIAM␈α
Journal␈α
of␈αComputing␈↓,
␈↓ α∧␈↓␈↓ αdVol. 5, No. 3, pp. 414␈↓¬-␈↓426.

␈↓ α∧␈↓27.␈↓ αdZ. Manna and R. Waldinger [August 1977]
␈↓ α∧␈↓␈↓ αd␈↓↓The␈α↔automatic␈α↔synthesis␈α↔of␈α⊗recursive␈α↔programs␈↓,␈α↔Proceedings␈α↔of␈α↔the␈α⊗Fifth
␈↓ α∧␈↓␈↓ αdInternational␈αJoint␈αConference␈αon␈αArtificial␈αIntelligence,␈αCambridge,␈αMA,␈αpp.
␈↓ α∧␈↓␈↓ αd405␈↓¬-␈↓411.

␈↓ α∧␈↓28.␈↓ αdN. Dershowitz and Z. Manna [November 1977]
␈↓ α∧␈↓␈↓ αd␈↓↓The␈α∂evolution␈α∂of␈α∂programs:␈α∂ A␈α∂system␈α∂for␈α∂automatic␈α∂program␈α∂modification␈↓,␈α∞IEEE
␈↓ α∧␈↓␈↓ αdTransactions on Software Engineering, Vol. 3, No. 5, pp. 377␈↓¬-␈↓385.

␈↓ α∧␈↓29.␈↓ αdZ. Manna and A. Shamir [November 1977]
␈↓ α∧␈↓␈↓ αd␈↓↓The␈α⊃optimal␈↓␈↓¬-␈↓␈↓↓fixedpoint␈α⊂approach␈α⊃to␈α⊂recursive␈α⊃programs␈↓,␈α⊃␈↓αCommunications␈α⊂ of


␈↓"β␈↓ α∧␈↓␈↓ εj7␈↓ d


␈↓"β␈↓ α∧␈↓α␈↓ αdthe␈α⊂ACM␈↓,␈α⊂Vol.␈α⊂20,␈α⊂No.␈α⊂11,␈α∂pp.␈α⊂824␈↓¬-␈↓831.␈α⊂ Also␈α⊂in␈α⊂␈↓↓Perspective␈α⊂on␈α∂Computer
␈↓ α∧␈↓↓␈↓ αdScience␈↓ (A. K. Jones, editor), ␈↓αAcademic Press␈↓, 1977, pp. 103␈↓¬-␈↓124.

␈↓ α∧␈↓30.␈↓ αdZ. Manna and R. Waldinger [February 1978]
␈↓ α∧␈↓␈↓ αd␈↓↓Is␈α⊂"sometime"␈α⊂sometimes␈α⊂better␈α⊂than␈α⊂always?␈α⊂ Intermittent␈α⊂assertions␈α⊂in␈α⊂proving
␈↓ α∧␈↓↓␈↓ αdprogram␈α⊗correctness␈↓,␈α⊗␈↓αCommunications␈α⊗of␈α⊗the␈α∃ACM␈↓,␈α⊗Vol.␈α⊗21,␈α⊗No.␈α⊗2,␈α∃pp.
␈↓ α∧␈↓␈↓ αd159␈↓¬-␈↓172.

␈↓ α∧␈↓31.␈↓ αdZ. Manna and A. Shamir [March 1978]
␈↓ α∧␈↓␈↓ αd␈↓↓The␈α
convergence␈αof␈α
functions␈αto␈α
fixedpoints␈αof␈α
recursive␈α
definitions␈↓,␈α␈↓αTheoretical
␈↓ α∧␈↓α␈↓ αdComputer Science Journal␈↓, Vol. 4, No. 1.

␈↓ α∧␈↓32.␈↓ αdZ. Manna and R. Waldinger [May 1978]
␈↓ α∧␈↓␈↓ αd␈↓↓The␈α≠logic␈α~of␈α≠computer␈α~programming␈↓,␈α≠␈↓αIEEE␈α~Transactions␈α≠on␈α~Software
␈↓ α∧␈↓α␈↓ αdEngineering␈↓, Vol. SE␈↓¬-␈↓4, No. 1.

␈↓ α∧␈↓33.␈↓ αdN. Dershowitz and Z. Manna [May 1978]
␈↓ α∧␈↓␈↓ αd␈↓↓Inference␈αrules␈αfor␈αprogram␈αannotation␈↓,␈αProceedings␈αof␈αthe␈αThird␈αInternational
␈↓ α∧␈↓␈↓ αdConference on Software Engineering, Atlanta, GA.

␈↓ α∧␈↓34.␈↓ αdZ. Manna and R. Waldinger [June 1978]
␈↓ α∧␈↓␈↓ αd␈↓↓The␈α~DEDALUS␈α~system␈↓,␈α≠Proceedings␈α~of␈α~the␈α~1978␈α≠National␈α~Computer
␈↓ α∧␈↓␈↓ αdConference. ␈↓αInvited paper␈↓.

␈↓ α∧␈↓35.␈↓ αdZ. Manna and R. Waldinger
␈↓ α∧␈↓␈↓ αd␈↓↓Synthesis␈↓:  ␈↓↓dreams␈↓ ␈↓ε=>␈↓ ␈↓↓programs␈↓, ␈↓αCommunications of the ACM␈↓ (to appear).


␈↓ α∧␈↓␈↓β⊗␈↓  ␈↓αBooks:␈↓

␈↓ α∧␈↓1.␈↓ αdZ. Manna [1973],
␈↓ α∧␈↓␈↓ αd␈↓↓Program␈α⊂schemas␈↓,␈α∂Chapter␈α⊂3␈α⊂in␈α∂␈↓αCurrents␈α⊂in␈α⊂the␈α∂theory␈α⊂of␈α⊂computing␈↓␈α∂(A.
␈↓ α∧␈↓␈↓ αdAho, editor), Prentice␈↓¬-␈↓Hall, Englewood Cliffs, NJ.

␈↓ α∧␈↓2.␈↓ αdZ. Manna [1974],
␈↓ α∧␈↓␈↓ αd␈↓αMathematical␈α≥theory␈α≥of␈α≥computation␈↓,␈α≥McGraw␈↓¬-␈↓Hill,␈α≥New␈α≡York,␈α≥NY.
␈↓ α∧␈↓␈↓ αd[Japanese␈αtranslation␈α
(1976),␈αInternational␈α
student␈αedition␈α
(1977),␈αItalian
␈↓ α∧␈↓␈↓ αdtranslation (1978), Russian translation (to appear)].

␈↓ α∧␈↓3.␈↓ αdZ. Manna and R. Waldinger (editors)[1977],
␈↓ α∧␈↓␈↓ αd␈↓αStudies in automatic programming logic␈↓, American␈↓¬-␈↓Elsevier, New York, NY.

␈↓"β␈↓ α∧␈↓␈↓ εj8␈↓ d


␈↓"β␈↓ α∧␈↓4.␈↓ αdZ. Manna and R. Waldinger,
␈↓ α∧␈↓␈↓ αdA␈α∞textbook␈α∞on␈α∞program␈α∞verification␈α∞and␈α∞synthesis,␈α∞program␈α∞transformation
␈↓ α∧␈↓␈↓ αdand optimization, and related topics.  In preparation.







































␈↓"β␈↓ α∧␈↓␈↓ εj9␈↓ d


␈↓"β␈↓ α∧␈↓␈↓ βQ␈↓αCOMMENTS ON MANNA'S MOST IMPORTANT PUBLICATIONS
␈↓ α∧␈↓α␈↓ β␈by John McCarthy, Professor of Computer Science␈↓

␈↓ α∧␈↓1. ␈↓↓Mathematical Theory of Computation␈↓, McGraw␈↓¬-␈↓Hill, New York 1974.

␈↓ α∧␈↓        This␈α∂book,␈α∞which␈α∂has␈α∂already␈α∞been␈α∂translated␈α∂into␈α∞Japanese,␈α∂Italian␈α∂and␈α∞Russian
␈↓ α∧␈↓and␈α_reprinted␈α_as␈α_a␈α_paperback,␈α→is␈α_the␈α_first␈α_textbook␈α_in␈α_mathematical␈α→theory␈α_of
␈↓ α∧␈↓computation.␈α Its␈αappearance␈αis␈αa␈αmajor␈αstep␈αtowards␈αreplacing␈α
experimental␈αdebugging
␈↓ α∧␈↓of computer programs by proofs that they meet their specifications.

␈↓ α∧␈↓        At␈αpresent,␈α
computer␈αprograms␈α
are␈αdebugged.␈α
 That␈αis,␈α
after␈αa␈α
program␈αis␈αwritten␈α
it
␈↓ α∧␈↓is␈α⊂tried␈α⊂on␈α⊂test␈α∂cases␈α⊂until␈α⊂its␈α⊂author␈α∂is␈α⊂satisfied␈α⊂and␈α⊂turns␈α∂it␈α⊂over␈α⊂to␈α⊂users.␈α⊂ If␈α∂the
␈↓ α∧␈↓program␈α
is␈α∞at␈α
all␈α∞complex,␈α
the␈α∞users␈α
usually␈α
find␈α∞further␈α
mistakes.␈α∞ Mistakes␈α
turn␈α∞up␈α
in
␈↓ α∧␈↓big␈α
systems␈αfor␈α
years.␈α
 The␈αmistakes␈α
often␈α
cause␈αeconomic␈α
loss␈α
and␈αthe␈α
cost␈α
of␈αfixing
␈↓ α∧␈↓them often exceeds the cost of the original program many times over.

␈↓ α∧␈↓        The␈α∃major␈α∃applied␈α⊗goal␈α∃of␈α∃mathematical␈α∃theory␈α⊗of␈α∃computation␈α∃is␈α⊗to␈α∃replace
␈↓ α∧␈↓debugging␈αby␈αmathematically␈αproving␈αthat␈α
the␈αprogram␈αmeets␈αits␈αspecifications.␈α
 Such␈αa
␈↓ α∧␈↓proof␈α∪must␈α∪then␈α∪be␈α∀checked␈α∪either␈α∪by␈α∪a␈α∀person␈α∪or␈α∪by␈α∪a␈α∀proof␈↓¬-␈↓checking␈α∪computer
␈↓ α∧␈↓program.␈α∪ Once␈α∪this␈α∩has␈α∪been␈α∪done,␈α∪the␈α∩chance␈α∪of␈α∪error␈α∪is␈α∩reduced␈α∪to␈α∪that␈α∪of␈α∩an
␈↓ α∧␈↓incongruity␈αbetween␈αthe␈αformal␈αspecifications␈αand␈αwhat␈αthe␈αusers␈αhave␈αin␈αmind␈αor␈αto␈αan
␈↓ α∧␈↓error␈α⊂in␈α∂the␈α⊂proof␈↓¬-␈↓checking␈α∂program␈α⊂or␈α⊂on␈α∂the␈α⊂part␈α∂of␈α⊂the␈α∂human␈α⊂checking␈α⊂the␈α∂proof.
␈↓ α∧␈↓Computer␈αscientists␈αbelieve␈αthat␈αformal␈αproving␈αwill␈αbring␈αabout␈αa␈αmajor␈αreduction␈αin␈αthe
␈↓ α∧␈↓cost of getting good programs.

␈↓ α∧␈↓        Manna's␈α∀text␈α∪is␈α∀the␈α∪first␈α∀big␈α∪step␈α∀in␈α∪making␈α∀these␈α∪techniques␈α∀accessible␈α∪to
␈↓ α∧␈↓students␈α∂of␈α∂computer␈α∞science␈α∂at␈α∂an␈α∂early␈α∞stage.␈α∂ Writing␈α∂the␈α∞first␈α∂textbook␈α∂in␈α∂a␈α∞new
␈↓ α∧␈↓field␈αis␈αa␈αmajor␈αcreative␈αendeavor,␈αand␈αManna's␈αbook␈αis␈αnot␈αa␈αmere␈αsummary␈αof␈αresearch
␈↓ α∧␈↓papers.␈α
 The␈α
high␈αregard␈α
the␈α
computer␈αscience␈α
world␈α
has␈αfor␈α
the␈α
book␈αis␈α
shown␈α
by␈αthe
␈↓ α∧␈↓number of translations into foreign languages.

␈↓ α∧␈↓        It␈α⊃is␈α⊃a␈α⊃first␈α⊃class␈α⊃scholarly␈α⊃work␈α⊃in␈α⊃that␈α⊃it␈α⊃reworks␈α⊃and␈α⊃presents␈α⊃not␈α∩only␈α⊃the
␈↓ α∧␈↓approaches␈α∂to␈α∂program␈α∂proving␈α∂that␈α∂Manna␈α∂himself␈α∂has␈α∂worked␈α∂on,␈α∂but␈α∂also␈α∂the␈α∞other
␈↓ α∧␈↓major␈αapproaches␈αand␈αnecessary␈αbackground␈αmaterial␈αfrom␈αmathematical␈αlogic,␈αrecursive
␈↓ α∧␈↓function theory and the theory of automata.

␈↓ α∧␈↓2.␈α∃"Properties␈α∃of␈α∃programs␈α∃and␈α∃the␈α∃first␈↓¬-␈↓order␈α∃predicate␈α∃calculus",␈α∃␈↓↓Journal␈α∃of␈α∃the
␈↓ α∧␈↓↓Association for Computing Machinery␈↓, Vol. 16, No. 2, pp. 244␈↓¬-␈↓255. April 1969.

␈↓ α∧␈↓        This␈α
paper,␈α
based␈α
on␈α
Manna's␈α
Ph.D.␈α
thesis,␈α
shows␈α
how␈α
to␈α
write␈α
sentences␈α
of␈α
the


␈↓"β␈↓ α∧␈↓␈↓ εa10␈↓ d


␈↓"β␈↓ α∧␈↓predicate␈α
calculus␈α
expressing␈α
the␈α
␈↓↓total␈α
correctness␈↓␈α
of␈αa␈α
program.␈α
 It␈α
is␈α
a␈α
kind␈α
of␈α
dual␈αto␈α
the
␈↓ α∧␈↓method␈α∃of␈α∃inductive␈α∃assertions␈α∃invented␈α∃by␈α∃Robert␈α∃Floyd␈α∃which␈α∃gives␈α∃only␈α∀partial
␈↓ α∧␈↓correctness,␈α⊃i.e.␈α⊃that␈α∩the␈α⊃program␈α⊃give␈α⊃correct␈α∩results␈α⊃under␈α⊃the␈α⊃assumption␈α∩that␈α⊃it
␈↓ α∧␈↓terminates.␈α∂ Manna's␈α∂new␈α∞method␈α∂is␈α∂a␈α∞creative␈α∂achievement␈α∂and␈α∂elegantly␈α∞presented,
␈↓ α∧␈↓but␈α∃ the␈α∃Manna␈α∃sentences␈α⊗have␈α∃been␈α∃difficult␈α∃to␈α⊗prove.␈α∃ The␈α∃method␈α∃is␈α⊗ripe␈α∃for
␈↓ α∧␈↓re␈↓¬-␈↓examination␈α_now␈α_that␈α_the␈α_techniques␈α_for␈α_proving␈α_such␈α_sentences␈α_are␈α_better
␈↓ α∧␈↓developed.

␈↓ α∧␈↓3.␈α⊗␈↓¬-␈↓␈α⊗with␈α⊗S.␈α⊗Ness␈α⊗and␈α∃J.␈α⊗Vuillemin,␈α⊗"Inductive␈α⊗methods␈α⊗for␈α⊗proving␈α⊗properties␈α∃of
␈↓ α∧␈↓programs", ␈↓↓Communications of the ACM␈↓, vol. 16, No. 8, ppl 491␈↓¬-␈↓502. (1973).

␈↓ α∧␈↓        This␈αpaper,␈αwhich␈α
won␈αan␈αACM␈αaward␈α
as␈αthe␈αbest␈α
paper␈αof␈α1974,␈αpresents␈α
several
␈↓ α∧␈↓methods␈α∞for␈α∞proving␈α
properties␈α∞of␈α∞both␈α
recursive␈α∞and␈α∞sequential␈α
programs.␈α∞ One␈α∞of␈α
the
␈↓ α∧␈↓methods␈α
has␈α
been␈α
revived␈α
by␈α
Morris␈α∞and␈α
Wegbreit␈α
under␈α
the␈α
name␈α
of␈α∞␈↓↓subgoal␈α
induction␈↓.
␈↓ α∧␈↓This␈α⊂method␈α⊂is␈α⊂for␈α∂recursive␈α⊂programs␈α⊂what␈α⊂Floyd's␈α∂inductive␈α⊂assertion␈α⊂method␈α⊂is␈α∂for
␈↓ α∧␈↓sequential programs.

␈↓ α∧␈↓4.␈α⊂␈↓¬-␈↓␈α⊂with␈α⊂R.␈α⊂Waldinger,␈α⊃"Is␈α⊂"sometimes"␈α⊂sometimes␈α⊂better␈α⊂than␈α⊃always?␈α⊂ Intermittent
␈↓ α∧␈↓assertions␈α
in␈α
proving␈α
program␈α
correctness",␈α
␈↓↓Communications␈α
of␈α
the␈α
ACM␈↓,␈α
vol.␈α
21,␈α
No.␈α2,␈α
pp.
␈↓ α∧␈↓159␈↓¬-␈↓172.  (February 1978).

␈↓ α∧␈↓        The␈αpaper␈αsuggests␈αa␈αnew␈αtechnique␈αfor␈αprogram␈αverification␈αwhich␈αallows␈αsimpler
␈↓ α∧␈↓and more intuitive proofs of many program properties including termination.

␈↓ α∧␈↓        The␈α
paper␈α∞has␈α
had␈α∞a␈α
substantial␈α
impact␈α∞on␈α
program␈α∞verification␈α
research␈α∞since␈α
it
␈↓ α∧␈↓was␈α⊂first␈α⊂presented␈α∂at␈α⊂the␈α⊂Second␈α∂International␈α⊂Conference␈α⊂on␈α⊂Software␈α∂Engineering
␈↓ α∧␈↓(October␈α1976).␈α
 Many␈αrecent␈α
papers␈αdiscuss␈α
the␈αtechnique,␈α
and␈αseveral␈αattempts␈α
have
␈↓ α∧␈↓been made to formalize the method.



␈↓ α∧␈↓␈↓β⊗␈↓  ␈↓αCurrent Research␈↓

␈↓ α∧␈↓Manna's␈α∀current␈α∀research␈α∀is␈α∀in␈α∪three␈α∀areas␈α∀␈↓¬-␈↓␈α∀mathematical␈α∀theory␈α∀of␈α∪computation,
␈↓ α∧␈↓computer program synthesis, and other topics in theoretical computer science.

␈↓ α∧␈↓        Manna␈α
has␈α
been␈α
one␈α
of␈α
the␈α
leaders␈α
in␈α
mathematical␈α
theory␈α
of␈α
computation␈α
since␈α
his
␈↓ α∧␈↓thesis␈α⊃in␈α⊃1968.␈α⊃ He␈α⊃continues␈α⊃to␈α⊃develop␈α⊃new␈α⊃techniques␈α⊃for␈α⊃proving␈α⊃that␈α⊂computer
␈↓ α∧␈↓programs␈α∀meet␈α∪their␈α∀specifications.␈α∪ Thus,␈α∀in␈α∪collaboration␈α∀with␈α∪his␈α∀student␈α∪Nachum
␈↓ α∧␈↓Dershowitz,␈αhe␈α
has␈αjust␈α
completed␈αa␈α
paper␈αshowing␈α
how␈αproduction␈αsystem␈α
computations


␈↓"β␈↓ α∧␈↓␈↓ εa11␈↓ d


␈↓"β␈↓ α∧␈↓can␈α∂be␈α∂proved␈α∂to␈α∂terminate␈α⊂by␈α∂induction␈α∂on␈α∂generalized␈α∂lexicographic␈α⊂orderings.␈α∂ This
␈↓ α∧␈↓has settled several previously recalcitrant cases.

␈↓ α∧␈↓        Within␈α⊃the␈α⊃last␈α⊃two␈α⊃years␈α⊃Manna␈α⊃has␈α⊃entered␈α⊃a␈α⊃new␈α⊃research␈α⊃area␈α⊃␈↓¬-␈↓␈α⊂program
␈↓ α∧␈↓synthesis.␈α
 He␈αis␈α
trying␈αto␈α
find␈α
relationships␈αamong␈α
existing␈αverification␈α
methods␈α
and␈αto
␈↓ α∧␈↓develop␈α∃new␈α∃ones.␈α∀ Related␈α∃efforts␈α∃are␈α∀aimed␈α∃at␈α∃the␈α∀automation␈α∃of␈α∃many␈α∃of␈α∀the
␈↓ α∧␈↓processes␈α∂a␈α∂programmer␈α∂usually␈α∂performs␈α∂by␈α∂hand␈α∂such␈α∂as␈α⊂debugging,␈α∂documentation,
␈↓ α∧␈↓modification␈α∂and␈α∞optimization.␈α∂ An␈α∞ultimate␈α∂goal␈α∂of␈α∞this␈α∂research␈α∞is␈α∂the␈α∂development␈α∞of
␈↓ α∧␈↓synthesis techniques, by which the entire programming task is performed automatically.

␈↓ α∧␈↓        If␈α
this␈αwork␈α
goes␈αwell,␈α
it␈αwill␈α
establish␈αtighter␈α
connection␈αbetween␈α
Stanford␈αwork␈α
in
␈↓ α∧␈↓theory of computation and the work in artificial intelligence.






























␈↓"β␈↓ α∧␈↓␈↓ εa12␈↓ d


␈↓"β␈↓ α∧␈↓␈↓ ¬1␈↓αIV. THE CANDIDATE'S ROLE␈↓

␈↓ α∧␈↓A. Description of candidate's expected role.

␈↓ α∧␈↓        Manna␈αwill␈αstrengthen␈αthe␈αComputer␈αScience␈αDepartment␈αin␈αmathematical␈αtheory␈αof
␈↓ α∧␈↓computation␈α∪and␈α∪program␈α∪synthesis.␈α∪ When␈α∪he␈α∪was␈α∪at␈α∪Stanford␈α∪before␈α∀he␈α∪directed
␈↓ α∧␈↓theses␈α∞in␈α∞mathematical␈α∂theory␈α∞of␈α∞computation,␈α∞and␈α∂his␈α∞careful␈α∞work␈α∞with␈α∂students␈α∞has
␈↓ α∧␈↓been␈αmissed.␈α He␈αwill␈αteach␈αthe␈αmain␈α
courses␈αand␈αtake␈αpart␈αin␈αcurriculum␈αdesign␈αin␈α
these
␈↓ α∧␈↓areas.

␈↓ α∧␈↓        We␈α∩also␈α⊃expect␈α∩him␈α∩to␈α⊃do␈α∩his␈α∩share␈α⊃of␈α∩committee␈α∩work,␈α⊃and␈α∩we␈α∩consider␈α⊃him
␈↓ α∧␈↓capable of taking his turn as department chairman.

␈↓ α∧␈↓B. He has already done all these things extremely successfully.

␈↓ α∧␈↓C.␈α
The␈α
department␈α
as␈α
a␈α
whole␈α
has␈α
connections␈α
with␈α
other␈α
departments,␈α
but␈α
Manna's␈α
field
␈↓ α∧␈↓is not especially involved in such collaborations.

␈↓ α∧␈↓D.␈α∪When␈α∀Manna␈α∪was␈α∀an␈α∪assistant␈α∀professor␈α∪here␈α∪at␈α∀Stanford␈α∪he␈α∀took␈α∪part␈α∀in␈α∪the
␈↓ α∧␈↓colloquium, library and curriculum committees.

␈↓ α∧␈↓At␈α∩the␈α⊃Weizmann␈α∩Institute,␈α∩he␈α⊃was␈α∩Head␈α⊃of␈α∩the␈α∩mathematics␈α⊃program␈α∩and␈α∩a␈α⊃council
␈↓ α∧␈↓member␈αof␈αthe␈α
Feinberg␈αGraduate␈αSchool.␈α
 He␈αhas␈αjust␈α
been␈αasked␈αto␈α
be␈αchairman␈αof␈α
the
␈↓ α∧␈↓Department of Applied Mathematics and Dean of the School of Mathematics.


















␈↓"β␈↓ α∧␈↓␈↓ εa13␈↓ d


␈↓"β␈↓ α∧␈↓␈↓ ¬"␈↓αV. EVALUATION OF TEACHING␈↓

␈↓ α∧␈↓␈↓β⊗␈↓  ␈↓αPh.D. Students:␈↓

␈↓ α∧␈↓Jean␈↓¬-␈↓Marie Cadion (1972)
␈↓ α∧␈↓␈↓↓Recursive Definitions of Partial Functions and their Computations␈↓

␈↓ α∧␈↓Ashok Chandra (1973)
␈↓ α∧␈↓␈↓↓On the Properties and Applications of Program Schemas␈↓

␈↓ α∧␈↓Jean Vuillemin (1973)
␈↓ α∧␈↓␈↓↓Proof Techniques for Recursive Programs␈↓

␈↓ α∧␈↓Shmuel Katz (1976)
␈↓ α∧␈↓␈↓↓Invariants and the Logical Analysis of Programs␈↓

␈↓ α∧␈↓Adi Shamir (1977)
␈↓ α∧␈↓␈↓↓Fixedpoints of Recursive Programs␈↓

␈↓ α∧␈↓Nachum Dershowitz (1978)
␈↓ α∧␈↓␈↓↓Automatic Program Modification␈↓

␈↓ α∧␈↓␈↓β⊗␈↓ ␈↓αEvaluation␈↓

␈↓ α∧␈↓        Manna␈α
is␈αan␈α
excellent␈α
lecturer␈αand␈α
is␈α
always␈αextremely␈α
well␈α
prepared.␈α Enclosed␈α
is
␈↓ α∧␈↓a␈α
copy␈α
of␈α
the␈α
student␈α
course␈α
evaluation␈α
of␈α
his␈α
most␈α
recent␈α
course␈α
taught␈α
at␈α
Stanford.␈α
 It
␈↓ α∧␈↓is␈αa␈αresearch␈αoriented␈αcourse␈αin␈αa␈αfield␈αin␈αwhich␈αmany␈αof␈αthe␈αstudents␈αwere␈αunprepared.
␈↓ α∧␈↓His␈α∩previous␈α∩courses␈α∩were␈α∩taught␈α∩before␈α∩the␈α∩Department␈α∩established␈α∪formal␈α∩course
␈↓ α∧␈↓evaluation, but his reputation at that time was excellent.













␈↓"β␈↓ α∧␈↓␈↓ εa14␈↓ d


␈↓"β␈↓ α∧␈↓␈↓ ¬d␈↓αVI. SEARCH REPORT␈↓

␈↓ α∧␈↓        The␈α→Computer␈α_Science␈α→Department␈α_has␈α→been␈α_trying␈α→to␈α_get␈α→an␈α_outstanding
␈↓ α∧␈↓researcher␈αand␈αteacher␈αin␈α
this␈αfield␈αfor␈αmany␈αyears.␈α
 In␈αour␈αletters␈αconcerning␈αManna␈α
we
␈↓ α∧␈↓asked␈α
for␈αcomparison␈α
with␈αthe␈α
outstanding␈α
people␈αin␈α
the␈αworld,␈α
including␈α
Anthony␈αHoare
␈↓ α∧␈↓and Dana Scott of Oxford, Edsger Dijkstra, and Rod Burstall of Edinburgh.

␈↓ α∧␈↓        Scott␈α∩was␈α∩previously␈α∪at␈α∩Stanford␈α∩in␈α∩the␈α∪Mathematics␈α∩Department␈α∩and␈α∪left␈α∩for
␈↓ α∧␈↓Princeton␈α∞and␈α∞finally␈α∞Oxford.␈α∞ His␈α∞field␈α
overlaps␈α∞Manna's␈α∞slightly,␈α∞but␈α∞his␈α∞strengths␈α
are
␈↓ α∧␈↓different.␈α∪ He␈α∩concentrates␈α∪more␈α∩on␈α∪logic␈α∩and␈α∪philosophy␈α∩and␈α∪his␈α∩computer␈α∪work␈α∩is
␈↓ α∧␈↓further␈αfrom␈αapplication.␈α We␈αdon't␈αknow␈αwhy␈αhe␈αleft␈αStanford,␈αbut␈αthere␈αis␈αno␈αreason␈αto
␈↓ α∧␈↓suppose␈α
he␈αwants␈α
to␈αreturn.␈α
 Whether␈αthe␈α
Department␈αwould␈α
prefer␈αhim␈α
if␈αwere␈α
available
␈↓ α∧␈↓has not been explored.

␈↓ α∧␈↓        Hoare␈α⊃visited␈α⊃Stanford␈α⊃in␈α⊂1973␈↓¬-␈↓74␈α⊃and␈α⊃his␈α⊃interest␈α⊂in␈α⊃coming␈α⊃to␈α⊃Stanford␈α⊂was
␈↓ α∧␈↓explored␈α∞with␈α∞negative␈α∂result;␈α∞instead␈α∞he␈α∞moved␈α∂from␈α∞Belfast␈α∞to␈α∞Oxford.␈α∂ Whether␈α∞we
␈↓ α∧␈↓would now prefer him is unexplored.

␈↓ α∧␈↓        Dijkstra␈α∂declined␈α∂a␈α∂Stanford␈α∂offer␈α⊂about␈α∂five␈α∂years␈α∂ago.␈α∂ The␈α⊂Department␈α∂would
␈↓ α∧␈↓definitely␈α
not␈α
make␈α
him␈α
an␈αoffer␈α
today,␈α
because␈α
of␈α
a␈αconviction␈α
that␈α
he␈α
is␈α
not␈αkeeping␈α
up
␈↓ α∧␈↓with what others have accomplished in this field.

␈↓ α∧␈↓        Burstall's␈α∩interest␈α∩in␈α⊃coming␈α∩to␈α∩Stanford␈α∩was␈α⊃explored␈α∩several␈α∩years␈α∩ago␈α⊃with
␈↓ α∧␈↓negative␈α∞results.␈α∞ Whether␈α
we␈α∞would␈α∞prefer␈α
him,␈α∞were␈α∞he␈α
available,␈α∞has␈α∞not␈α∞been␈α
fully
␈↓ α∧␈↓explored, but the general opinion is that we would prefer Manna.

␈↓ α∧␈↓        If␈α
either␈α
Scott␈α
or␈αHoare␈α
were␈α
available,␈α
we␈αwould␈α
probably␈α
consider␈α
them␈αtargets
␈↓ α∧␈↓of opportunity.

␈↓ α∧␈↓        In␈α∀our␈α∀letters,␈α∀we␈α∀asked␈α∀for␈α∀recommendations␈α∀of␈α∀competitive␈α∃candidates␈α∀and
␈↓ α∧␈↓received none.

␈↓ α∧␈↓        We␈α⊂are␈α∂confident␈α⊂that␈α∂we␈α⊂know␈α⊂everyone␈α∂who␈α⊂has␈α∂made␈α⊂major␈α⊂contributions␈α∂to
␈↓ α∧␈↓mathematical theory of computation.

␈↓ α∧␈↓        None of the outstanding people in this field are candidates for affirmative action.



␈↓ α∧␈↓We␈α∂are␈α∂considering␈α∞the␈α∂appointment␈α∂of␈α∞Manna␈α∂as␈α∂a␈α∞new␈α∂appointment␈α∂although␈α∂he␈α∞has


␈↓"β␈↓ α∧␈↓␈↓ εa15␈↓ d


␈↓"β␈↓ α∧␈↓been␈α
here␈α
before.␈α However,␈α
because␈α
he␈αhas␈α
been␈α
here␈αbefore,␈α
 the␈α
senior␈αfaculty␈α
know
␈↓ α∧␈↓Manna's work very well and unanimously support the appointment.








































␈↓"β␈↓ α∧␈↓␈↓ εa16␈↓ d